Serveur d'exploration sur la recherche en informatique en Lorraine

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems

Identifieur interne : 007597 ( Main/Exploration ); précédent : 007596; suivant : 007598

A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems

Auteurs : Stephan Merz ; Martin Wirsing ; Julia Zappe

Source :

RBID : CRIN:merz03a

English descriptors

Abstract

We define a variant of Lamport's Temporal Logic of Actions, extended by spatial modalities, that is intended for the specification of mobile systems with distributed state. We discuss notions of refinement appropriate for mobile systems, specifically concerning the topological structure of the system, and show how these can be represented in the logic via quantification and implication, ensuring transitivity and compositionality of refinements.


Affiliations:


Links toward previous steps (curation, corpus...)


Le document en format XML

<record>
<TEI>
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en" wicri:score="421">A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems</title>
</titleStmt>
<publicationStmt>
<idno type="RBID">CRIN:merz03a</idno>
<date when="2003" year="2003">2003</date>
<idno type="wicri:Area/Crin/Corpus">003795</idno>
<idno type="wicri:Area/Crin/Curation">003795</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">003795</idno>
<idno type="wicri:Area/Crin/Checkpoint">000B28</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000B28</idno>
<idno type="wicri:Area/Main/Merge">007975</idno>
<idno type="wicri:Area/Main/Curation">007597</idno>
<idno type="wicri:Area/Main/Exploration">007597</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title xml:lang="en">A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems</title>
<author>
<name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
</author>
<author>
<name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name>
</author>
<author>
<name sortKey="Zappe, Julia" sort="Zappe, Julia" uniqKey="Zappe J" first="Julia" last="Zappe">Julia Zappe</name>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc>
<textClass>
<keywords scheme="KwdEn" xml:lang="en">
<term>mobile systems</term>
<term>refinement</term>
<term>spatial logic</term>
<term>specification</term>
<term>temporal logic</term>
<term>tla</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en" wicri:score="1937">We define a variant of Lamport's Temporal Logic of Actions, extended by spatial modalities, that is intended for the specification of mobile systems with distributed state. We discuss notions of refinement appropriate for mobile systems, specifically concerning the topological structure of the system, and show how these can be represented in the logic via quantification and implication, ensuring transitivity and compositionality of refinements.</div>
</front>
</TEI>
<affiliations>
<list></list>
<tree>
<noCountry>
<name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
<name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name>
<name sortKey="Zappe, Julia" sort="Zappe, Julia" uniqKey="Zappe J" first="Julia" last="Zappe">Julia Zappe</name>
</noCountry>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 007597 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 007597 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     CRIN:merz03a
   |texte=   A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems
}}

Wicri

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022